A, B, C:Realizer. R-icompat(A;B  C)  (R-icompat(A;B) & R-icompat(A;C)) 

latex

Definitions	, P  Q, P  Q, tt, ff, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), if b then t else f fi , Y, x. t(x), t  T, P & Q, R-icompat(A;B), P  Q, x:A. B(x), x(s), Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rnone(), , left  right
Lemmas	Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, es realizer wf, Rnone wf, R-icompat wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf